/*
 * SYmbolic Model-Based test case generation toOL for Real-Time systems (SYMBOLRT)
 * (C) Copyright 2010-2012 Federal University of Campina Grande (UFCG)
 * 
 * This file is part of SYMBOLRT.
 *
 * SYMBOLRT is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * SYMBOLRT is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with SYMBOLRT.  If not, see <http://www.gnu.org/licenses/>.
 *
 *
 * REVISION HISTORY:
 * Author                           Date           Brief Description
 * -------------------------------- -------------- ------------------------------
 * Wilkerson de Lucena Andrade      16/06/2011     An old class named TIOSTSPreprocessing (Version 1.2) was divided into two classes. This class only contains the synchronous algorithm algorithm (Version 1.0).
 * 
 */

package br.edu.ufcg.symbolrt.algorithms;

import java.util.Collection;
import java.util.List;

import br.edu.ufcg.symbolrt.base.Action;
import br.edu.ufcg.symbolrt.base.Location;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.Transition;
import br.edu.ufcg.symbolrt.base.TypedData;
import br.edu.ufcg.symbolrt.symbolicexecution.exception.IncompatibleOperationException;
import br.edu.ufcg.symbolrt.util.Constants;


/**
 * <code>SynchronousProduct</code> Class. <br>
 * This class contains an algorithm needed to perform the sequential composition between two TIOSTSs.
 * 
 * @author Adriana Carla Damasceno  ( <a href="mailto:adriana@copin.ufcg.edu.br">adriana@copin.ufcg.edu.br</a> )
 * 
 * @version 1.0
 * <br>
 * SYmbolic Model-Based test case generation toOL for Real-Time systems (SYMBOLRT)
 * <br>
 * (C) Copyright 2010-2012 Federal University of Campina Grande (UFCG)
 * <br>
 * <a href="https://sites.google.com/a/computacao.ufcg.edu.br/symbolrt">https://sites.google.com/a/computacao.ufcg.edu.br/symbolrt</a>
 */
public class SequentialCompositionShared {

	private static SequentialCompositionShared instance = null;


	private SequentialCompositionShared() {
	}


	/**
	 * Method used to obtain an instance of this class.
	 * @return An instance of {@link SequentialCompositionShared}.
	 */
	public static SequentialCompositionShared getInstance() {
		if (instance == null) {
			instance = new SequentialCompositionShared();
		}
		return instance;
	}

	/**
	 * Returns the sequential composition between two TIOSTSs.
	 * @param t1 The first TIOSTS.
	 * @param t1 The second TIOSTS.
	 * @return The sequential composition between t1 and t2.
	 * @throws IncompatibleSequentialComposition If t1 do not fit conditions demanded to it.  
	 */
	public TIOSTS sequentialComposition(TIOSTS tiosts1, TIOSTS tiosts2, String name) throws IncompatibleOperationException {

		TIOSTS result;

		Location lc = getCompositionLocation(tiosts1);

		if (!isCompatible(tiosts1, tiosts2, lc)){
			throw new IncompatibleOperationException("The set of variables, locations and clocks from both TIOSTSs must be disjoint and the final node must not contain one or more transitions.");
		}
		else{

			result = initialize(tiosts1, tiosts2, name);
			//Building the new set of transitions

			result.addTransitions(tiosts1.getTransitions());
			result.addTransitions(tiosts2.getTransitions());				
			List<Transition> initialTransitions = tiosts2.getInitialLocation().getOutTransitions();

			//Creating new transitions from the composition location of tiosts1 to the sucessors of the initial node of tiosts2
			for(Transition t:initialTransitions){
				t.setSource(lc);
			}
		}

		return result;
	}

	private TIOSTS initialize (TIOSTS tiosts1, TIOSTS tiosts2, String name){
		TIOSTS result = new TIOSTS(name);

		List<Action> internalActions;
		List<Action> outputActions;
		List<Action> inputActions;
		List<TypedData> variables;
		List<TypedData> parameters;
		List<String> clocks;
		result.setInitialCondition(tiosts1.getInitialCondition());
		result.setInitialLocation(tiosts1.getInitialLocation());

		//Performing union between internal, input and output actions
		internalActions = tiosts1.getInternalActions();
		internalActions.addAll(tiosts2.getInternalActions());
		result.setInternalActions(internalActions);

		outputActions = tiosts1.getOutputActions();
		outputActions.addAll(tiosts2.getOutputActions());
		result.setOutputActions(outputActions);

		inputActions = tiosts1.getInputActions();
		inputActions.addAll(tiosts2.getInputActions());			
		result.setInputActions(inputActions);

		//Performing union between variables, parameters and clocks of t1 and t2
		variables = tiosts1.getVariables();
		variables.addAll(tiosts2.getVariables());
		result.setVariables(variables);

		parameters = tiosts1.getActionParameters();
		parameters.addAll(tiosts2.getActionParameters());
		result.setActionParameters(parameters);	

		clocks = tiosts1.getClocks();
		clocks.addAll(tiosts2.getClocks());
		result.setClocks(clocks);

		//Performing the union between locations of tiosts1 and tiosts2
		for (Location l: tiosts1.getLocations()){
			result.addLocation(l);
		}		
		for (Location l: tiosts2.getLocations()){
			if (!l.isInitialLocation()){
				result.addLocation(l);	
			}								
		}

		return result;
	}

	private boolean isCompatible(TIOSTS tiosts1, TIOSTS tiosts2, Location lc) throws IncompatibleOperationException{
		boolean resp = false;

		if (lc != null){
			List<Transition> outputTransitionslc =  lc.getOutTransitions();
			if (outputTransitionslc.isEmpty() && intersection(tiosts1.getLocationNames(), tiosts2.getLocationNames()) == false && intersection(tiosts1.getClocks(), tiosts2.getClocks()) == false && intersection(tiosts1.getvariableNames(), tiosts2.getvariableNames()) == false){
				resp = true;
			}		
		}else{
			resp = false;
		}

		return resp;
	}


	private Location getCompositionLocation(TIOSTS tiosts) throws IncompatibleOperationException{
		Collection<Transition> transitions = tiosts.getTransitions();
		Collection<Location> locations = tiosts.getLocations();

		Location compositeLocation = null;
		for(Location l: locations){					

			//Verifies if the current location l is source of a transition
			boolean foundOutgoingTransition = false;				
			for(Transition t:transitions){
				if (t.getSource() == l){
					foundOutgoingTransition = true;
				}
			}

			//If there is no location without outgoing transitions found, l is the one
			if (compositeLocation == null && foundOutgoingTransition == false){
				compositeLocation = l;
			}else{
				// If a location without outgoing transitions was found, the TIOSTS has more than one composite location, being out of our restrictions 
				if (compositeLocation != null && foundOutgoingTransition == false){
					throw new IncompatibleOperationException("Only one location without outgoing transitions is allowed");
				}
			}				
		}

		return compositeLocation;

	}

	private boolean intersection(List<String> colecao1, List<String> colecao2){
		boolean isIntersection = false;

		for (String c:colecao1){
			if (colecao2.contains(c)){
				isIntersection = true;
			}
		}		

		return isIntersection;
	}

}